FDL - Nuprl Lemma : strong-subtype-set

Nuprl Lemma : strong-subtype-set

A,B:Type.
strong-subtype(A; B)

(

P:(A

prop{i:l}), Q:(B

prop{i:l}).

(

x:A. P(x)

Q(x))

strong-subtype({x:A| P(x)} ; {x:B| Q(x)} ))

Definitions strong-subtype(A; B), f(a), x(s), prop{i:l}, {x:A| B(x)} , x:A. B(x), P Q, x:A. B(x), x:AB(x), s = t, Type, A c B, t T, x:A B(x), True, T